00100	COMMENT$ Here is a set of first order axioms for the integers based on
00200	the successor operation written SUCC and the predecessor operation
00300	written PRED.  While the axioms don't mention sets, they are compatible
00400	with a later imbedding into set theory, because the SORT mechanism of
00500	FOL relativizes the axioms to the domain NATNUM, so other domains are
00600	possible.  These axioms contain more than is logically necessary in
00700	order to make proofs easier.$
01300	
01400	
01500	DECLARE INDVAR I I1 I2 I3 J J1 J2 J3
01600	K K1 K2 K3 L L1 L2 L3
01700	M M1 M2 M3 N N1 N2 N3
01800	 ε NATNUM;
01900	DECLARE OPCONST SUCC: NATNUM → NATNUM [PRE];
02000	DECLARE OPCONST PRED: NATNUM → INTEGER [PRE];
02100	DECLARE INDVAR X Y Z;
02200	DECLARE PREDPAR P(NATNUM);
02300	
02400	
02500	AXIOM PRED:	∀N.(¬N=0 ⊃ NATNUM(PRED N));;
02600	
02700	AXIOM PEANO:	∀N.(¬SUCC N = 0),
02800			∀N.PRED SUCC N = N,
02900			∀N.(¬N=0 ⊃ SUCC PRED N = N);;
03000	
03100	AXIOM ONE:	SUCC 0 = 1;;
03200	
03300	AXIOM INDUCTION:P(0) ∧ ∀N.(P(N) ⊃ P(SUCC N)) ⊃ ∀N.P(N);;
03400	
03500	
03600	COMMENT$ The rest of these axioms are really just definitions.$
03700	
03800	DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM[R←475,L←470];
03900	DECLARE PREDCONST ≥(NATNUM,NATNUM)[INF];
03950	DECLARE PREDCONST >(NATNUM,NATNUM)[INF];
04000	DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM[R←555,L←550];
04100	DECLARE OPCONST -(NATNUM,NATNUM)=INTEGER[R←455,L←450];
04200	
04300	AXIOM PLUS:	∀M.(M+0=M),
04400			∀M N.(M+SUCC N =SUCC(M+N)),
04500			∀M N.(M+N=N+M)
04600			∀M N K.M+(N+K)=(M+N)+K
04700	;;
04800	
04900	AXIOM TIMES:	∀M. M*0=0,
05000			∀M.M*1=1,
05100			∀M N. M*SUCC N = M*N+M,
05200			∀M N. M*N=N*M,
05300			∀M N K. M*(N*K)=(M*N)*K
05400	;;
05500	
05600	AXIOM DISTRIB:	∀M N K.M*(N+K)=M*N+M*K;;
05700	
05800	
05900	AXIOM MINUS:	∀M N. (M ≥ N ⊃ NATNUM(M-N)),
06000			∀M. M-0 = M,
06100			∀M N. (M - SUCC N = PRED(M - N)),
06200			∀N.N-N=0,
06300			∀M N K.(M+N)-K=M+(N-K);;
06400	
06500	
06600	AXIOM GREATER:	∀M. M≥0,
06700			∀M. (0≥M ⊃ M=0),
06800			∀M N. (M≥N ≡ PRED M ≥ PRED N),
06900			∀M N.(M>N ≡ M≥N ∧ ¬(M=N)),
07000			∀M N.(M≥N ≡ ∃K.(M=N+K)),
07100			∀M N K. (M>N ∧ N≥K ⊃ M>K),
07200			∀M N K. (M≥N ∧ N>K ⊃ M>K),
07300			∀M N K. (M≥N ∧ N≥K ⊃ M≥K);;